Statecharts, “From Visual Syntax to ModelTheoretic Semantics

This paper presents a novel model–theoretic account of Harel, Pnueli and Shalev’s original step semantics of the visual specification language Statecharts. The graphical syntax of a Statechart is read, directly and structurally, as a formula in propositional logic. This proposition cap-tures all the logical constraints imposed by the diagram on the Statechart’s semantics, i.e., the possible sets of transitions that can be taken together to perform a valid Statecharts step, and their effects on Statecharts config-urations. The paper’s main result shows that the correct semantics is uniquely described by the intuitionistic in-terpretation of Statecharts formulas, whereas the naive classical interpretation is insufficient. The advocated in-tuitionistic approach not only gives a correct, clear and direct logical account of Statecharts ’ semantics, but also permits the integration of Statecharts with formal valida-tion tools, such as theorem provers